package src.graph;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;
import java.util.Map.Entry;

import src.util.MiniMap;
import src.util.MiniSet;

import checkers.javari.quals.ReadOnly;
import checkers.javari.quals.PolyRead;
import checkers.nullness.quals.NonNull;
import checkers.nullness.quals.Nullable;
import checkers.quals.DefaultLocation;
import checkers.quals.DefaultQualifier;
@DefaultQualifier(value = "checkers.nullness.quals.NonNull", locations =
{ DefaultLocation.ALL_EXCEPT_LOCALS })
public class GraphCopier {

	public /*@ReadOnly*/ Graph copy(/*@ReadOnly*/Graph g) {
		Graph copy = new Graph();
		/*@ReadOnly*/MiniSet<String> nodes = g.nodes();
		for (String nodeId : nodes) {
			copy.addNode(nodeId);
		}
		
		
		/*@ReadOnly*/MiniMap<String, /*@ReadOnly*/MiniSet<String>> edges = g.edges();
		for (String nodeId: nodes) {
			/*@ReadOnly*/MiniSet<String> image = edges.get(nodeId);
			if (image == null)
				copy.addUniv(nodeId);
			else {
				for (String to : image) {
					copy.addEdge(nodeId, to);
				}
			}
		}
		return copy;
	}
	
}
